m:, n:m. upto(m)[n] = n   

latex

Definitions	SQType(T), {T}, ij, i<j, hd(l), t  ...$L, P  Q, ij, S  T, , upto(n), Unit, P  Q, i=j, ||as||, , b, Prop, b, i  j < k, AB, P & Q, A, False, P  Q, l[i], Dec(P), P  Q, {i..j}, x:A. B(x), t  T
Lemmas	decidable lt, assert wf, not wf, bnot wf, length wf2, select wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, int seg wf, upto wf, length wf1, nat wf, nat properties, ge wf, le wf, length upto, select append front, non neg length, length cons, length nil, select append back